$\forall$$E$, $T$:Type, $x$:($T$$\times$$T$). tree\_node($x$) $\in$ tree\_con($E$;$T$)